Nuprl Lemma : map_length
11,40
postcript
pdf
A
,
B
:Type,
f
:(
A
B
),
as
:(
A
List). ||map(
f
;
as
)|| = ||
as
||
latex
Definitions
t
T
,
Y
,
map(
f
;
as
)
,
||
as
||
,
x
:
A
.
B
(
x
)
origin
A,B:Type, f:(A
B), as:(A List). ||map(f; as)|| = ||as|| 
A,B:Type, f:(AB), as:(A List). ||map(f; as)|| = ||as|| Tx:A. B(x)